﻿package 
{



	public class Btree
	{
		public const ANDS:String = "&";
		public const ORS:String = "|";
		public const NOTS:String = "¬";
		public const IMPS:String = "→";

		public var btreeRoot:Node;

		public function Btree(inp:String)
		{
			inp = stripspaces(inp);
			btreeRoot = new Node();

			parseOperators(inp,this.btreeRoot);


			implFree(btreeRoot);
			removeDoubleNeg(this.btreeRoot);
			introduceNegation(btreeRoot);
			removeDoubleNeg(this.btreeRoot);
			btreeRoot = cnf(btreeRoot);

			optim(btreeRoot);
			//trace(buildCNFString(btreeRoot));
			//trace(this.nodeToString(btreeRoot));
		}


		public function buildCNFString(node:Node):String
		{
			var sym:String = new String();
			var returnString:String = new String();
			var i:int = 0;
			var j:int = 0;
			var minCharCode:int = 256;
			var numVars:int = 0;
			var numCl:int = (node.contents.length+1)/2;
			//trace(node.contents.length);
			for (i=0; i<node.contents.length; i++)
			{
				if (i % 2 == 0)
				{
					if (node.contents[i].contents.length > numVars)
					{

						numVars = node.contents[i].contents.length;
					}
					for (j=0; j<node.contents[i].contents.length; j++)
					{
						if (j % 2 == 0)
						{

							if (node.contents[i].contents[j].val != null && node.contents[i].contents[j].val != NOTS)
							{
								if (sym.search(node.contents[i].contents[j].val) == -1)
								{
									sym +=  node.contents[i].contents[j].val;
								}


								if (minCharCode > node.contents[i].contents[j].val.charCodeAt(0))
								{
									minCharCode = node.contents[i].contents[j].val.charCodeAt(0);
								}
							}
							else if (node.contents[i].contents[j].val == NOTS)
							{

								if (sym.search(node.contents[i].contents[j].val) == -1)
								{
									sym +=  node.contents[i].contents[j].val;
								}

								if (minCharCode > node.contents[i].contents[1].val.charCodeAt(0))
								{
									minCharCode = node.contents[i].contents[1].val.charCodeAt(0);
								}

							}
							else if(node.contents[i].val!=null) {
								if (sym.search(node.contents[i].val) == -1)
								{
									sym +=  node.contents[i].val;
								}

								if (minCharCode > node.contents[i].val.charCodeAt(0))
								{
									minCharCode = node.contents[i].val.charCodeAt(0);
								}
							}
							else if(node.contents[i].val==null && node.contents[i].contents[0] == NOTS) {
								if (sym.search(node.contents[i].contents[1].val) == -1)
								{
									sym +=  node.contents[i].contents[1].val;
								}

								if (minCharCode > node.contents[i].contents[1].val.charCodeAt(0))
								{
									minCharCode = node.contents[i].contents[1].val.charCodeAt(0);
								}
							}
							else
							{
								if (sym.search(node.contents[i].contents[j].contents[1].val) == -1)
								{
									sym +=  node.contents[i].contents[j].contents[1].val;
								}

								if (minCharCode > node.contents[i].contents[j].contents[1].val.charCodeAt(0))
								{

									minCharCode = node.contents[i].contents[j].contents[1].val.charCodeAt(0);
								}
							}
						}
					}
				}

			}



			numVars = sym.length;
			//trace(numIn);
			//trace(numOut);

			var lineStr:String = "c Made by Marcin Glombiowski \np cnf " + numVars + " " + numCl + " \n";
			returnString+=lineStr.slice(0);
			lineStr = "";
			var addedChar:String = new String();

			for (i=0; i<node.contents.length; i++)
			{
				if (i % 2 == 0)
				{
					for (j=0; j<node.contents[i].contents.length; j++)
					{
						if (j % 2 == 0)
						{


							if (node.contents[i].contents[j].val != null && node.contents[i].contents[j].val != NOTS)
							{
								addedChar = String(node.contents[i].contents[j].val.charCodeAt(0) + 1 - minCharCode);
								
								
							}
							else if (node.contents[i].contents[j].val == NOTS)
							{
								addedChar = "-" + String(node.contents[i].contents[1].val.charCodeAt(0) + 1 - minCharCode);
								
								
							}
							else if(node.contents[i].val!=null) {
								addedChar = String(node.contents[i].val.charCodeAt(0) + 1 - minCharCode);
							}
							else if(node.contents[i].val==null && node.contents[i].contents[0] == NOTS) {
								addedChar = "-" + String(node.contents[i].contents[1].valcharCodeAt(0) + 1 - minCharCode);
							}
							else
							{

								addedChar = "-" + String(node.contents[i].contents[j].contents[1].val.charCodeAt(0) + 1 - minCharCode);

	
							}
							//if(lineStr.indexOf(addedChar)==-1) {
								lineStr +=  addedChar;
								lineStr +=  " ";
								//}
							
						}



					}
					lineStr +=  "0 \n";
					returnString+=lineStr.slice(0);
					lineStr = "";

				}


			}
			return returnString;
		}





		private function optim(node:Node)
		{


			for (var i:int=0; i<node.contents.length; i++)
			{
				if (i % 2 == 0)
				{

					if (node.contents[i].val == null && node.contents[1].val == node.contents[i].contents[1].val)
					{
						//trace(node.contents[1].val);
						var newCont:Array = new Array();
						var lowerArray:Array = new Array();

						lowerArray = lowerArray.concat(node.contents[i].contents);

						newCont = node.contents.slice(0,i);
						newCont = newCont.concat(lowerArray);
						newCont = newCont.concat(node.contents.slice(i + 1));

						node.contents = newCont;
						optim(node);
						break;
					} else {
						optim(node.contents[i]);
					}


					
				}
			}











		}

		public function stripspaces(originalstring:String):String
		{
			var original:Array = originalstring.split(" ");
			return (original.join(""));
		}

		private function parseOperators(inp:String, node:Node, sym:String="")
		{


			var nodeLeft:Node = new Node();
			var symbolNode:Node = new Node();
			var nodeRight:Node = new Node();

			var newRightNode:Node = new Node();

			var leftNodeCont:String;
			var rightNodeCont:String;
			nodeLeft.father = node;
			nodeRight.father = node;
			symbolNode.father = node;
			var level:int = 0;
			var depth:int = 0;
			var lastI:int = node.contents.length - 1;

			var complex:Boolean = false;


			for (var i:int = 0; i<inp.length; i++)
			{

				if (inp.charAt(i) == "(")
				{

					depth +=  1;
				}
				else if (inp.charAt(i)==")")
				{

					depth -=  1;
					if (depth == 0 && i != inp.length - 1)
					{

						complex = true;
					}
					if (depth == 0 && i == inp.length - 1 && complex == false)
					{
						if (inp.charAt(0) == "(" && inp.charAt(i) == ")")
						{
							inp = inp.slice(1,inp.length - 1);
							parseOperators(inp, node);
							break;
						}
					}
				}


				if (depth == 0)
				{
					if (level == 0)
					{



						if (inp.charAt(i) == IMPS)
						{

							symbolNode.val = inp.charAt(i);

							node.contents.push(nodeLeft);
							node.contents.push(symbolNode);
							node.contents.push(nodeRight);

							leftNodeCont = inp.slice(0,i);
							rightNodeCont = inp.slice(i + 1);


							if (anySigns(leftNodeCont))
							{
								parseOperators(leftNodeCont, nodeLeft);
							}
							else
							{
								nodeLeft.val = leftNodeCont;
							}


							if (anySigns(rightNodeCont))
							{
								parseOperators(rightNodeCont, nodeRight);
							}
							else
							{
								nodeRight.val = rightNodeCont;
							}


							break;
						}
						else if (i==inp.length-1)
						{
							i = -1;
							level = 1;
						}

					}
					else if (level == 1)
					{

						if (inp.charAt(i) == ORS)
						{

							symbolNode.val = inp.charAt(i);

							node.contents.push(nodeLeft);
							node.contents.push(symbolNode);
							node.contents.push(nodeRight);

							leftNodeCont = inp.slice(0,i);
							rightNodeCont = inp.slice(i + 1);

							if (anySigns(leftNodeCont))
							{

								parseOperators(leftNodeCont, nodeLeft);

							}
							else
							{
								nodeLeft.val = leftNodeCont;
							}


							if (anySigns(rightNodeCont))
							{

								parseOperators(rightNodeCont, nodeRight);

							}
							else
							{
								nodeRight.val = rightNodeCont;


							}

							break;

						}
						else if (i==inp.length-1)
						{
							i = -1;
							level = 2;
						}

					}
					else if (level == 2)
					{

						if (inp.charAt(i) == ANDS)
						{



							symbolNode.val = inp.charAt(i);

							node.contents.push(nodeLeft);
							node.contents.push(symbolNode);
							node.contents.push(nodeRight);

							leftNodeCont = inp.slice(0,i);
							rightNodeCont = inp.slice(i + 1);

							if (anySigns(leftNodeCont))
							{
								parseOperators(leftNodeCont, nodeLeft);
							}
							else
							{
								nodeLeft.val = leftNodeCont;
							}


							if (anySigns(rightNodeCont))
							{

								parseOperators(rightNodeCont, nodeRight);

							}
							else
							{

								nodeRight.val = rightNodeCont;
							}

							break;

						}
						else if (i==inp.length-1)
						{
							i = -1;
							level = 3;
						}

					}
					else if (level==3 && inp.charAt(i)==NOTS)
					{

						symbolNode.val = NOTS;
						rightNodeCont = inp.slice(i + 1);

						node.contents.push(symbolNode);
						node.contents.push(nodeRight);
						if (anySigns(rightNodeCont))
						{
							parseOperators(rightNodeCont, nodeRight);
						}
						else
						{
							nodeRight.val = rightNodeCont;
						}

						break;
					}
				}


			}

		}

		private function cnf(node:Node):Node
		{

			if (node.val == null)
			{
				if (node.contents[1].val == ANDS)
				{

					node.contents[0] = cnf(node.contents[0]);
					node.contents[2] = cnf(node.contents[2]);
					return node;

				}
				else if (node.contents[1].val==ORS)
				{

					return distr(cnf(node.contents[0]), cnf(node.contents[2]));

				}

			}

			return node;
		}

		private function distr(node1:Node, node2:Node):Node
		{

			var leftNode:Node = new Node();
			var rightNode:Node = new Node();

			var symbolNode:Node = new Node();

			var newNode:Node = new Node();
			if (node1.val == null && node1.contents[1].val == ANDS)
			{

				leftNode = distr(node1.contents[0],node2);
				rightNode = distr(node1.contents[2],node2);
				symbolNode.val = ANDS;


			}
			else if (node2.val==null && node2.contents[1].val == ANDS)
			{

				leftNode = distr(node1,node2.contents[0]);
				rightNode = distr(node1,node2.contents[2]);
				symbolNode.val = ANDS;

			}
			else
			{
				symbolNode.val = ORS;
				leftNode = node1;
				rightNode = node2;
			}


			newNode.contents.push(leftNode);
			newNode.contents.push(symbolNode);
			newNode.contents.push(rightNode);

			return newNode;



		}

		public function nodeToString(node:Node):String
		{

			var retString:String = "";
			if (node.val == null)
			{
				for (var i:int=0; i<node.contents.length; i++)
				{

					if (node.contents[i].val == null)
					{
						retString +=  "(" + nodeToString(node.contents[i]) + ")";
					}
					else
					{
						retString +=  node.contents[i].val;
					}

				}
			}
			else
			{
				retString = node.val;
			}

			return retString;
		}

		private function removeDoubleNeg(node:Node)
		{
			var changed:Boolean = false;

			if (node.contents[0]!=null && node.contents[0].val == NOTS && node.contents[1].contents[0] != null)
			{
				if (node.contents[1].contents[0].val == NOTS)
				{
					node.val = node.contents[1].contents[1].val;
					node.contents = node.contents[1].contents[1].contents;
					changed = true;
					removeDoubleNeg(node);
				}
				
			} 
			if(changed==false) {
			for (var i:int=0; i<node.contents.length; i++)
			{

				if (node.contents[i] != null && node.contents[i].val == null)
				{
					removeDoubleNeg(node.contents[i]);
				}

			}
			}
			



		}


		private function neg(node:Node):Node
		{
			var ret:Node = new Node();
			var newNegNode:Node = new Node();
			newNegNode.father = node.father;

			var negation:Node = new Node();
			var negatedNode:Node = new Node();

			negation.father = newNegNode;
			negation.val = NOTS;

			negatedNode.father = newNegNode;

			negatedNode = node.cloneMe();

			ret = newNegNode;

			newNegNode.contents.push(negation);
			newNegNode.contents.push(negatedNode);


			return ret;

		}

		private function implFree(node:Node)
		{

			if (node.val == null && node.contents[1].val == IMPS)
			{


				node.contents[0] = neg(node.contents[0]);
				node.contents[1].val = ORS;


				implFree(node.contents[0]);


				implFree(node.contents[2]);


			}
			else if (node.val==null && node.contents.length>2)
			{

				for (var i:int=0; i<node.contents.length; i++)
				{

					if (i % 2 == 0)
					{
						implFree(node.contents[i]);
					}

				}

			}
			else if (node.val==null && node.contents.length==2)
			{
				implFree(node.contents[1]);
			}


		}

		private function introduceNegation(node:Node)
		{
			var i:int = 0;

			if (node.contents[0] != null && node.contents[0].val == NOTS)
			{

				if (node.contents[1].val == null)
				{
					if (node.contents[1].contents[1].val == ANDS || node.contents[1].contents[1].val == ORS)
					{
						if (node.contents[1].contents[1].val == ANDS)
						{
							node.contents[1].contents[1].val = ORS;
						}
						else
						{
							node.contents[1].contents[1].val = ANDS;
						}

						for (i= 0; i<node.contents[1].contents.length; i++)
						{
							if (i % 2 == 0)
							{

								node.contents[1].contents[i] = neg(node.contents[1].contents[i]);

								introduceNegation(node.contents[1].contents[i]);
							}
						}
						node.val = node.contents[1].val;
						node.contents = node.contents[1].contents;

					}


				}
			}

			if (node.contents.length > 1)
			{


				for (i = 0; i<node.contents.length; i++)
				{

					if (node.contents[i].val == null)
					{
						introduceNegation(node.contents[i]);
					}
				}

			}

		}

		private function anySigns(inp:String):Boolean
		{
			if (inp.indexOf(")") != -1 || inp.indexOf("(") != -1 || inp.indexOf(IMPS) != -1 || inp.indexOf(NOTS) != -1 || inp.indexOf(ORS) != -1 || inp.indexOf(ANDS) != -1)
			{
				return true;
			}
			else
			{
				return false;
			}


		}

	}

}